(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const r2 Real)
(declare-const r4 Real)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v13 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert (or (or v3 v10 (<= 0.0 r2 1211.0 579100.0) v10 (= (- (- (+ 637568.0 r4 0.0))) (+ (+ 637568.0 r4 0.0) (- (+ 637568.0 r4 0.0))) (- 1211.0)) (distinct (xor (>= 1211.0 r4 637568.0 r2) v9 v4 v3 (<= 0.0 r2 1211.0 579100.0) (<= 0.0 r2 1211.0 579100.0) v11 v5 v9 (<= 0.0 r2 1211.0 579100.0) (=> v9 (= r2 0.0 r2 r2))) v2 v1 v8 v9 v3 (=> v9 (= r2 0.0 r2 r2)) v3 v3)) v19 (or v3 v10 (<= 0.0 r2 1211.0 579100.0) v10 (= (- (- (+ 637568.0 r4 0.0))) (+ (+ 637568.0 r4 0.0) (- (+ 637568.0 r4 0.0))) (- 1211.0)) (distinct (xor (>= 1211.0 r4 637568.0 r2) v9 v4 v3 (<= 0.0 r2 1211.0 579100.0) (<= 0.0 r2 1211.0 579100.0) v11 v5 v9 (<= 0.0 r2 1211.0 579100.0) (=> v9 (= r2 0.0 r2 r2))) v2 v1 v8 v9 v3 (=> v9 (= r2 0.0 r2 r2)) v3 v3))))
(assert (or v13 v19 v19))
(assert (or v19 v13 (or v3 v10 (<= 0.0 r2 1211.0 579100.0) v10 (= (- (- (+ 637568.0 r4 0.0))) (+ (+ 637568.0 r4 0.0) (- (+ 637568.0 r4 0.0))) (- 1211.0)) (distinct (xor (>= 1211.0 r4 637568.0 r2) v9 v4 v3 (<= 0.0 r2 1211.0 579100.0) (<= 0.0 r2 1211.0 579100.0) v11 v5 v9 (<= 0.0 r2 1211.0 579100.0) (=> v9 (= r2 0.0 r2 r2))) v2 v1 v8 v9 v3 (=> v9 (= r2 0.0 r2 r2)) v3 v3))))
(assert (or v19 v13 (or v3 v10 (<= 0.0 r2 1211.0 579100.0) v10 (= (- (- (+ 637568.0 r4 0.0))) (+ (+ 637568.0 r4 0.0) (- (+ 637568.0 r4 0.0))) (- 1211.0)) (distinct (xor (>= 1211.0 r4 637568.0 r2) v9 v4 v3 (<= 0.0 r2 1211.0 579100.0) (<= 0.0 r2 1211.0 579100.0) v11 v5 v9 (<= 0.0 r2 1211.0 579100.0) (=> v9 (= r2 0.0 r2 r2))) v2 v1 v8 v9 v3 (=> v9 (= r2 0.0 r2 r2)) v3 v3))))
(check-sat)
